Aiming at the safety verification problem of a class of stochastic continuous system equipped with both random initial state and stochastic differential equation, a new computation method based on stochastic barrier certificates and initial set selection was proposed. Firstly, the related knowledge and concepts of stochastic continuous system and its safety verification were introduced. Then, it was discussed that how to determine the initial state set for the initial variables obeying several different distributions. The safety verification problem was converted into the polynomial optimization problem by using the method of stochastic barrier certificates according to the selected initial state set. Finally, the sum of squares relaxation method was used to transform the problem into sum of squares programming problem, and the lower bound of safety probability was obtained by using the SOSTOOLS tool. The theoretical analysis and experimental results show that, the proposed method has the complexity of polynomial time and can effectively compute the lower bound of safety probability for stochastic continuous system in unbounded time.

The research methods of mechanical geometry theorem proving were summed up into two categories, deterministic algorithms and probabilistic algorithms, and then an improved probabilistic algorithm was proposed to overcome the drawbacks such as poor efficiency or memory consumption in the existing methods. That was, the upper bounds of the degrees of variables in the pseudo-remainder were estimated by adopting an improved algorithm, and then on the basis of combining Schwartz-Zippel theorem and statistical theory, a geometric theorem could be proved by checking several random instances, the probability of error result could also be calculated and controlled within any given small range. Through the improved probabilistic algorithm, the Five Circles Theorem had already been proved successfully within two seconds which is quite difficult to be proved by existing algebra methods for its high complexity. Comparative experiment results also show that the improved probabilistic algorithm is high efficient.

To study the reachability of a class of nonlinear hybrid systems, this paper presented an verification method based on polyhedron inclusion. Firstly, some notions about hybrid systems and reachability were introduced. The method based on polyhedron inclusion was proposed to compute the linear approximation of polynomial hybrid systems. Quantifier elimination and nonlinear optimization method were applied to obtain the associated linear hybrid systems. Then the over-approximation of reachable set of original polynomial hybrid systems can be computed by using SpaceEx. Furthermore, the safety properties of the systems also can be verified.